\begin{tabbing}
$M$.rframe($k$ reads $x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}val(\=IdDeq;\+
\\[0ex]1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of($M$)))))))))));
\\[0ex]$x$;
\\[0ex]$x$,$L$.deq{-}member(KindDeq;$k$;$L$))
\-
\end{tabbing}